Section: New Results

Formal proofs of Tarjan's strongly connected components algorithm

Participants : Cyril Cohen, Laurent Théry, Ran Chen [Institute of Software, Chinese Academy of Science, Beijing] , Jean-Jacques Lévy [Inria Paris, $\pi .r^2$ project-team] , Stephan Merz [Inria Nancy Grand Est, Veridis project-team] .

Comparing provers on a formalization of the same problem is always a valuable exercise. In this work, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle. This was published in an international conference [8].